#include "formulagenerator.h"
#include "schemacomponentformula.h"
#include "schema.h"
#include "schemacomponent.h"
#include "formula.h"
#include "table.h"
#include "view.h"
#include "symbolicVariable.h"
#include "truthValue.h"
#include "tablecolumn.h"
#include "simplequery.h"
#include "querytree.h"
#include "from.h"
#include "fromcomponent.h"
#include "tablecolumnlist.h"
#include "expression.h"
#include "where.h"
#include "columnReference.h"
#include "logicUnaryOperation.h"
#include "logicBinaryOperation.h"
#include "numericBinaryOperation.h"
#include "numericUnaryOperation.h"
#include "select.h"
#include "columnlist.h"
#include "existsExpression.h"
#include "substitution.h"
#include "checkconstraint.h"

#include <stdio.h>
#include <iostream>
#include <stack>
using namespace std;

FormulaGenerator::FormulaGenerator(Schema * schema)
{
    generated = new map<string, SchemaComponentFormula *>();
    this->schema = schema;
}

FormulaGenerator::~FormulaGenerator()
{
    map<string,SchemaComponentFormula *>::iterator it;
	for(it = generated->begin(); it != generated->end(); it++){
		delete (*it).second;
	}//for
	delete generated; generated = NULL;
}

void FormulaGenerator::setSchema(Schema * schema)
{
    this->schema = schema;
}

bool FormulaGenerator::generateFormulaFor(const string & name, SchemaComponentFormula * & formula)
{
    SchemaComponent * component = NULL;

    // Gets the component from the schema.
    if(!schema->get(name,component)){
        formula = NULL;
        return false;
    }// if

    // Tests if the Formula has already been generated.
    map<string, SchemaComponentFormula *>::iterator it;
    it = generated->find(name);
    if(it == generated->end()){

        generate(name);
        //component->generateFormula(this);

        // Test if the Formula could be generated.
        it = generated->find(name);
        if(it == generated->end()){
            formula = NULL;
            return false;
        }// if
    }// if
    formula = (*it).second;
    return true;
}

void FormulaGenerator::generate(const string & component_name)
{
    SchemaComponent * component = NULL;
    // Gets the component from the schema.
    if(schema->get(component_name,component)){
        // Tests if the Formula has already been generated.
        map<string, SchemaComponentFormula *>::iterator it;
        it = generated->find(component_name);
        if(it == generated->end()){
            // component->generateFormula(this);
            SchemaComponentFormula * schema_component_formula = generate(component);
            if(schema_component_formula != NULL){
                generated->insert(pair<string, SchemaComponentFormula *>(component->getName(), schema_component_formula));
            }// if
        }// if
    }// if-else
}

SchemaComponentFormula * FormulaGenerator::generate(SchemaComponent * schema_component)
{
    Table * table = dynamic_cast<Table *>(schema_component);
    if(table != NULL) return generate(table);
    View * view = dynamic_cast<View *>(schema_component);
    if(view != NULL) return generate(view);
    return NULL;
}

SchemaComponentFormula * FormulaGenerator::generate(Table * table)
{
	SchemaComponentFormula * formula = new SchemaComponentFormula();
	formula->setSchemaComponent(table->getName());

    // TEMP
    cout << "Please, set the number of rows for table " + table->getName() + ": ";
    int rows = 1;
    cin >> rows;
    table->setRows(rows);
    //
    //BooleanExpression * constrExp = NULL;
    vector<BooleanExpression * > * constrExp = new vector<BooleanExpression*>();
    TableConstraintList * tconstrl = table->getConstraints();
    if (tconstrl!=NULL){
        vector<TableConstraint *> * constr = tconstrl->getTableConstraints();
        if (constr!=NULL){
            for (unsigned int j=0;j<constr->size();j++){
	      BooleanExpression * b1 = generate(constr->at(j),table);
	      constrExp->push_back(b1);
            }
        }
    }


    for(int i=0; i<table->getRows(); i++){
      Formula * f = new Formula();
      if(constrExp==NULL){
	TruthValue * truth = new TruthValue(True);
	f->setExpression(truth);
	delete truth; truth = NULL;
      }
      else {
	TruthValue * truth = new TruthValue(True);
	f->setExpression(truth);
	delete truth; truth = NULL;
	//f->setExpression(constrExp);
      }
      TableColumnList * tcl = table->getTableColumns();
      vector<TableColumn *> * c = tcl->getColumns();
      for(unsigned int j=0; j<c->size(); j++){
	string str = table->getName() + "." + c->at(j)->getName();
	SymbolicVariable * to_add = new SymbolicVariable(table->getName(),c->at(j)->getName(),i,c->at(j)->getType());
	f->addSubstitution(str,to_add);
	delete to_add; to_add = NULL;
      }//for



      formula->addFormula(f);
      formula->setTableConstraints(constrExp,table->getName());
    }//for

    return formula;
}
BooleanExpression * FormulaGenerator::generate(TableConstraint * constraint, Table * table)
{
  BooleanExpression * response;
  PrimaryKeyConstraint * pkc = dynamic_cast<PrimaryKeyConstraint *> (constraint);
  if (pkc!=NULL){
    response = generate(pkc, table);
    return response;
  }

  ForeignKeyConstraint * fkc = dynamic_cast<ForeignKeyConstraint *> (constraint);
  if (fkc!=NULL){
    response = generate(fkc, table);
    return response;
  }
  CheckConstraint * chc = dynamic_cast<CheckConstraint *> (constraint);
  if (chc!=NULL){
    chc->setTableName(table->getName());
    response = generate(chc,table);
    return response;
  }
}

BooleanExpression * FormulaGenerator::generate(CheckConstraint * chc, Table * table){
  BooleanExpression * ret = NULL;
  //TODO generar substitutions
  for (unsigned int i=0;i<table->getRows();i++){
  vector<Substitution * > * substitutions = new vector<Substitution *>();
  vector<FromComponent *> * from_components= new vector<FromComponent *>();
  from_components->push_back(new FromComponent(table->getName(),table->getName()));
    vector<Column*> * cols = table->getColumns()->getColumns();
    for (int j=0; j<cols->size(); j++){
      substitutions->push_back(new Substitution(table->getName()+"."+cols->at(j)->getName(),new SymbolicVariable(table->getName(),cols->at(j)->getName(),i,table->getColumnType(cols->at(j)->getName())))); 
      substitutions->push_back(new Substitution("."+cols->at(j)->getName(),new SymbolicVariable(table->getName(),cols->at(j)->getName(),i,table->getColumnType(cols->at(j)->getName()))));

    }
    Expression * expr = chc->getExpression();
    BooleanExpression * aux = dynamic_cast<BooleanExpression*>(replaceColumnReferenceByExpression(expr, substitutions, substitutions, from_components,from_components));
    if (ret==NULL && aux!=NULL) ret = aux;
    else if (ret!=NULL && aux!=NULL)ret = new LogicBinaryOperation(ret,"AND", aux);
    else fprintf(stderr,"Ups, something went wrong while generating Check Constraint Formula\n");
    
  }
  /* BooleanExpression * ret = NULL;
    
  for (unsigned int i=0;i<table->getRows();i++){
    Expression * expr = chc->getExpression();
    Expression * result = expr->clone();
    Expression * pointer = result;
    std::cout<<"table rows: " << table->getRows() <<"\n";
    SymbolicVariable * s = dynamic_cast<SymbolicVariable *>(pointer);
    ColumnReference * cr = dynamic_cast<ColumnReference *>(pointer);
    if(cr != NULL){
      if(cr->getTableId() == "") cr->setTableId(table->getName());
      pointer = new SymbolicVariable(table->getName(),cr->getColumnId(), i, table->getColumnType(cr->getColumnId()));
    }
    else if (s!=NULL){
      pointer = new SymbolicVariable(table->getName(),s->getColumnName(), i, table->getColumnType(s->getColumnName()));      
    }
    stack<Expression *> lifo;
    lifo.push(pointer);
    while(!lifo.empty()){
      pointer = lifo.top();
      lifo.pop();
      LogicBinaryOperation * lbe = dynamic_cast<LogicBinaryOperation *>(pointer);
      if(lbe != NULL){
	ColumnReference * crr = dynamic_cast<ColumnReference *>(lbe->getRightExpression());
	SymbolicVariable * s = dynamic_cast<SymbolicVariable *>(lbe->getRightExpression());

	if(crr != NULL || s != NULL){
	  Expression * substitution = NULL;
	  if(crr!=NULL){
	    if (crr->getTableId() == "") crr->setTableId(table->getName());
	    lbe->setRightExpression(new SymbolicVariable(table->getName(),crr->getColumnId(), i, table->getColumnType(crr->getColumnId())));}
	  else if (s!=NULL)
	    lbe->setRightExpression(new SymbolicVariable(table->getName(),s->getColumnName(), i, table->getColumnType(s->getColumnName())));

	  std::cout<<"g";
	}
	else{
	  lifo.push(lbe->getRightExpression());
	}// if-else
	ColumnReference * crl = dynamic_cast<ColumnReference *>(lbe->getLeftExpression());
	SymbolicVariable * sl = dynamic_cast<SymbolicVariable *>(lbe->getLeftExpression());
	if(crl != NULL){
	  Expression * substitution = NULL;
	  if(crl->getTableId() == "") crl->setTableId(table->getName());
	  lbe->setLeftExpression(new SymbolicVariable(table->getName(),crl->getColumnId(), i, table->getColumnType(crl->getColumnId())));
	}
	else if (sl!=NULL) 
	  lbe->setLeftExpression(new SymbolicVariable(table->getName(),sl->getColumnName(), i, table->getColumnType(sl->getColumnName())));
	else{
	  lifo.push(lbe->getLeftExpression());
	}// if-else
      }else{
	LogicUnaryOperation * lue = dynamic_cast<LogicUnaryOperation *>(pointer);
	if(lue != NULL){
	  ColumnReference * cr = dynamic_cast<ColumnReference *>(lue->getExpression());
	  SymbolicVariable * s = dynamic_cast<SymbolicVariable *>(lue->getExpression());
	  if(cr != NULL){
	    Expression * substitution = NULL;
	    if(cr->getTableId() == "")
	      lue->setExpression(new SymbolicVariable(table->getName(),cr->getColumnId(), i, table->getColumnType(cr->getColumnId())));
	    else lue->setExpression(new SymbolicVariable(cr->getTableId(),cr->getColumnId(), i, table->getColumnType(cr->getColumnId())));
	  }
	  else if (s!=NULL) 
	    lue->setExpression(new SymbolicVariable(table->getName(),s->getColumnName(), i, table->getColumnType(s->getColumnName())));
	  else{
	    lifo.push(lue->getExpression());
	  }// if-else
	}else{
	  NumericBinaryOperation * nbe = dynamic_cast<NumericBinaryOperation *>(pointer);
	  if(nbe != NULL){
	    ColumnReference * crr = dynamic_cast<ColumnReference *>(nbe->getRightExpression());
	    SymbolicVariable * s = dynamic_cast<SymbolicVariable *>(nbe->getRightExpression());
	    if(crr != NULL){
	      Expression * substitution = NULL;
	      if(crr->getTableId() == "")crr->setTableId(table->getName());
	      nbe->setRightExpression(new SymbolicVariable(table->getName(),crr->getColumnId(), i,table->getColumnType(crr->getColumnId())));
	    }
	    else if (s!=NULL)
	      nbe->setRightExpression(new SymbolicVariable(table->getName(),s->getColumnName(), i, table->getColumnType(s->getColumnName())));
	    else{
	      lifo.push(nbe->getRightExpression());
	    }// if-else
	    ColumnReference * crl = dynamic_cast<ColumnReference *>(nbe->getLeftExpression());
	    SymbolicVariable * sl = dynamic_cast<SymbolicVariable *>(nbe->getLeftExpression());
	    if(crl != NULL){
	      Expression * substitution = NULL;
	      if(crl->getTableId() == "")crl->setTableId(table->getName());
	      nbe->setLeftExpression(new SymbolicVariable(table->getName(),crl->getColumnId(), i, table->getColumnType(crl->getColumnId())));
	    }
	    else if (sl!=NULL)
	      nbe->setLeftExpression (new SymbolicVariable(table->getName(),sl->getColumnName(), i, table->getColumnType(sl->getColumnName())));
	    else{
	      lifo.push(nbe->getLeftExpression());
	    }// if-else
	  }else{
	    NumericUnaryOperation * nue = dynamic_cast<NumericUnaryOperation *>(pointer);
	    if(nue != NULL){
	      ColumnReference * cr = dynamic_cast<ColumnReference *>(nue->getExpression());
	      SymbolicVariable * s = dynamic_cast<SymbolicVariable *>(nue->getExpression());

	      if(cr != NULL){
		Expression * substitution = NULL;
		if(cr->getTableId() == "")cr->setTableId(table->getName());
		nue->setExpression(new SymbolicVariable(table->getName(),cr->getColumnId(), i, table->getColumnType(cr->getColumnId())));
	      }
	      else if (s!=NULL)
		nue->setExpression(new SymbolicVariable(table->getName(),s->getColumnName(), i, table->getColumnType(s->getColumnName())));
	      else{
		lifo.push(nue->getExpression());
	      }// if-else
	    }else{
	      // NOTHING TO DO
	    }// if-else
	  }// if-else
	}// if-else
      }//if-else
      }// while*//*
  if (ret==NULL) ret = dynamic_cast<BooleanExpression*> (result);
  else ret = new LogicBinaryOperation(ret,"and",result);
}
return ret;  */
  return ret;
}

BooleanExpression * FormulaGenerator::generate(PrimaryKeyConstraint * constraint, Table * table)
{
	SchemaComponentFormula * resp = new SchemaComponentFormula;
	ColumnList * cl= constraint->getColumns();
	vector<Column*> * cols= cl->getColumns();
	BooleanExpression * And1 = new TruthValue(True);
	for (unsigned int i=0;i<table->getRows();i++){
		BooleanExpression * And2 = new TruthValue(True);
		for (unsigned int j=i+1; j<table->getRows();j++){
			BooleanExpression * OrDifferent = NULL;
			if (cols->size()>0){
				SymbolicVariable * sv1 = new SymbolicVariable(table->getName(),cols->at(0)->getName(),i,table->getColumnType(cols->at(0)->getName()));
				SymbolicVariable * sv2 = new SymbolicVariable(table->getName(),cols->at(0)->getName(),j,table->getColumnType(cols->at(0)->getName()));
				OrDifferent = new  LogicBinaryOperation(sv1,"!=",sv2);

			}//if
			else OrDifferent = new TruthValue(True);
			for (unsigned int k=1; k<cols->size(); k++){
				SymbolicVariable * sv1 =new SymbolicVariable(table->getName(),cols->at(k)->getName(),i,table->getColumnType(cols->at(k)->getName()));
				SymbolicVariable * sv2 =new SymbolicVariable(table->getName(),cols->at(k)->getName(),j,table->getColumnType(cols->at(k)->getName()));
				BooleanExpression * b = new LogicBinaryOperation(sv1,"!=",sv2);
				OrDifferent = new LogicBinaryOperation(OrDifferent,"OR",b);
			}
		And2 = new LogicBinaryOperation(And2,"AND",OrDifferent);
		}
	And1 = new LogicBinaryOperation(And1,"AND",And2);
	}
	return And1;

}

BooleanExpression * FormulaGenerator::generate(ForeignKeyConstraint * constraint, Table * table)
{
	SchemaComponent * t2;
	const string referencedTableName = constraint->getTable();
	if(!schema->get(referencedTableName,t2)) return NULL;
	Table * tab2 = dynamic_cast<Table*>(t2);
	if (tab2==NULL) return NULL;

	map<string, SchemaComponentFormula *>::iterator it;
        it = generated->find(tab2->getName());
        if(it == generated->end()) generate(tab2->getName());

	ColumnList * cl= table->getColumns();
	vector<Column*> * cols= cl->getColumns();
	BooleanExpression * And1 = NULL;
	for (unsigned int i=0;i<table->getRows();i++){
		BooleanExpression * Or1 = NULL;
		//for (unsigned int j=0; j<table->getRows();j++){
		for (unsigned int j=0; j<tab2->getRows();j++){
			BooleanExpression * And2 = NULL;
			for (unsigned int k=0; k<cols->size(); k++){
					string referencedCol="";
					if (constraint->getReferencedColumn(cols->at(k)->getName(),referencedCol)){
						SymbolicVariable * sv1 =new SymbolicVariable(table->getName(),cols->at(k)->getName(),i,table->getColumnType(cols->at(k)->getName()));
						string refCol="";
						constraint->getReferencedColumn(cols->at(k)->getName(),refCol);
						SymbolicVariable * sv2 =new SymbolicVariable(tab2->getName(),refCol,j,tab2->getColumnType(refCol));
						BooleanExpression * b = new LogicBinaryOperation(sv1,"==",sv2);
						if (And2 ==NULL) And2=b;
						else And2 = new LogicBinaryOperation(And2,"AND",b);
				}
			}
		if(Or1==NULL) Or1 = And2;
		else Or1 = new LogicBinaryOperation(Or1,"OR",And2);
		}
	if(And1==NULL) And1 = Or1;
	else And1 = new LogicBinaryOperation(And1,"AND",Or1);
	}
	return And1;

}


SchemaComponentFormula * FormulaGenerator::generate(View * view)
{
    vector<FromComponent *> * upper_from_components = new vector<FromComponent *>();
    vector<Substitution *> * upper_substitutions = new vector<Substitution*>();

	SchemaComponentFormula * formula = generate(view->getQueryTree(),upper_substitutions,upper_from_components);

        for(unsigned int i=0; i<upper_from_components->size(); i++){
	    delete upper_from_components->at(i);
		}

	delete upper_from_components; upper_from_components = NULL;
	for(unsigned int i=0; i<upper_substitutions->size(); i++){
	  delete upper_substitutions->at(i);
	}
	delete upper_substitutions; upper_substitutions = NULL;

	formula->setSchemaComponent(view->getName());

	//	map<string, vector<BooleanExpression *> * > * table_constraints = formula->getTableConstraints();
	//	formula->setTableConstraints(table_constraints);

	// SUBSTITUTIONS
	//

	vector<Formula *> * row_formulas = formula->getAllFormulas();
	vector<Column *> * view_columns = view->getColumnList()->getColumns();

    for(unsigned int i=0; i<row_formulas->size(); i++){
        vector<Substitution *> * new_substitutions = new vector<Substitution *>();
        vector<Substitution *> * old_substitutions = row_formulas->at(i)->getSubstitutions();
        for(unsigned int j=0; j<view_columns->size(); j++){
            new_substitutions->push_back(new Substitution(view->getName()+"."+view_columns->at(j)->getName(),old_substitutions->at(j)->getSubstitution()));
        }//for

        row_formulas->at(i)->setSubstitutions(new_substitutions);

        for(unsigned int j=0; j<new_substitutions->size(); j++){
            delete new_substitutions->at(j);
        }
        delete new_substitutions; new_substitutions = NULL;
    }// for



	/*QueryTree * qt = view->getQueryTree();
    if(qt->getQueryType() == SIMPLE){

		SimpleQuery * sq = qt->getSimpleQuery();
		vector<Expression *> * select = sq->getSelect()->getSelectExpressions();
        vector<Formula *> * row_formulas = formula->getAllFormulas();
        vector<Column *> * view_columns = view->getColumnList()->getColumns();

        for(unsigned int i=0; i<row_formulas->size(); i++){
            vector<Substitution *> * new_substitutions = new vector<Substitution *>();
            vector<Substitution *> * old_substitutions = row_formulas->at(i)->getSubstitutions();
            for(unsigned int j=0; j<view_columns->size(); j++){
                bool finded = false;
                unsigned int k = 0;
                while(!finded && k<old_substitutions->size()){
                    if(old_substitutions->at(k)->getSubstituted() == select->at(j)->toString()){
                        finded = true;
                    }else k++;
                }//while
                new_substitutions->push_back(new Substitution(view->getName()+"."+view_columns->at(j)->getName(),old_substitutions->at(k)->getSubstitution()));
            }//for
            row_formulas->at(i)->setSubstitutions(new_substitutions);

            for(unsigned int j=0; j<new_substitutions->size(); j++){
                delete new_substitutions->at(j);
            }
            delete new_substitutions; new_substitutions = NULL;
        }// for

	}else if(qt->getQueryType() == UNION){

    }else if(qt->getQueryType() == INTERSECTION){

    }// if-else*/

	return formula;
}

SchemaComponentFormula * FormulaGenerator::generate(QueryTree * query_tree, vector<Substitution *> * upper_substitutions, vector<FromComponent *> * upper_from_components)
{
	if(query_tree->getQueryType() == SIMPLE){
		return generate(query_tree->getSimpleQuery(),upper_substitutions,upper_from_components);
	}else if(query_tree->getQueryType() == UNION){
		SchemaComponentFormula * left_formula = generate(query_tree->getLeftQueryTree(),upper_substitutions,upper_from_components);
		SchemaComponentFormula * right_formula = generate(query_tree->getRightQueryTree(),upper_substitutions,upper_from_components);
		vector<Formula *> * left = left_formula->getAllFormulas();
		vector<Formula *> * right = right_formula->getAllFormulas();

		SchemaComponentFormula * formula_union = new SchemaComponentFormula();
		for(int i=0; i<left->size(); i++){
            formula_union->addFormula(left->at(i)->clone());
		}// for

		for(int i=0; i<right->size(); i++){
            Formula * f = right->at(i)->clone();
            vector<Substitution *> * left_subs = left->at(0)->getSubstitutions();
            vector<Substitution *> * new_right_subs = f->getSubstitutions();
            for(unsigned int j=0; j<new_right_subs->size(); j++){
                new_right_subs->at(j)->setSubstituted(left_subs->at(j)->getSubstituted());
            }// for
            formula_union->addFormula(f);
            delete f; f = NULL;
		}// for

		delete left_formula; left_formula = NULL; left = NULL;
		delete right_formula; right_formula = NULL; right = NULL;

		return formula_union;

	}else if(query_tree->getQueryType() == INTERSECTION){
		SchemaComponentFormula * left_formula = generate(query_tree->getLeftQueryTree(),upper_substitutions,upper_from_components);
		SchemaComponentFormula * right_formula = generate(query_tree->getRightQueryTree(),upper_substitutions,upper_from_components);
		vector<Formula *> * left = left_formula->getAllFormulas();
		vector<Formula *> * right = right_formula->getAllFormulas();

		SchemaComponentFormula * formula_intersection = new SchemaComponentFormula();

        for(unsigned int i=0; i<left->size(); i++){
            vector<Substitution *> * left_subs_i = left->at(i)->getSubstitutions();
            for(unsigned int j=0; j<right->size(); j++){
                vector<Substitution *> * right_subs_j = right->at(j)->getSubstitutions();
                if(left_subs_i->size() == right_subs_j->size()){
                    bool equals = true;
                    unsigned int k=0;
                    while(equals && k<left_subs_i->size()){
                        if(left_subs_i->at(k)->toString() != right_subs_j->at(k)->toString()) equals = false;
                        k++;
                    }// for
                    if(equals){
                        vector<Formula *> * to_conjunction = new vector<Formula *>();
                        to_conjunction->push_back(left->at(i));
                        to_conjunction->push_back(right->at(j));
                        Expression * conjunction = createConjunction(to_conjunction);
                        Formula * f = new Formula();
                        f->setExpression(conjunction);
                        f->setSubstitutions(left_subs_i);
                        formula_intersection->addFormula(f);
                        delete to_conjunction; to_conjunction = NULL;
                        delete conjunction; conjunction = NULL;
                        delete f; f = NULL;
                    }// if
                }//if
            }// for
        }// for

        delete left_formula; left_formula = NULL; left = NULL;
		delete right_formula; right_formula = NULL; right = NULL;

		return formula_intersection;
	}else return NULL;
}

SchemaComponentFormula * FormulaGenerator::generate(SimpleQuery * query, vector<Substitution *> * upper_substitutions, vector<FromComponent *> * upper_from_components)
{
	SchemaComponentFormula * formula = new SchemaComponentFormula();

	vector<Expression *> * select_expressions = query->getSelect()->getSelectExpressions();
	vector<FromComponent *> * from_components = query->getFrom()->getComponents();
	Expression * where_expression = NULL;
	if(query->getWhere() != NULL) where_expression = query->getWhere()->getExpression();

	generateFromFormulas(from_components);
	vector<Formula *> * cartesian_product = calculateCartesianProduct(from_components);
	for(unsigned int i=0; i<from_components->size(); i++) {
	  formula->setTableConstraints(generated->find(from_components->at(i)->getName())->second->getTableConstraints());
	}
	if(where_expression != NULL){
	  for(unsigned int i=0; i<from_components->size(); i++) {
	    upper_from_components->push_back(from_components->at(i)->clone());
	  }
	    vector<Formula *> * where_formula = generateWhereFormula(where_expression,cartesian_product,upper_substitutions,from_components,upper_from_components);
	    computeQuerySubstitutions(where_formula,select_expressions,upper_substitutions,from_components,upper_from_components);
	    formula->setFormulas(where_formula);
	    for(unsigned int i=0; i<where_formula->size(); i++) delete where_formula->at(i);
	    delete where_formula; where_formula = NULL;
	    for(unsigned int i=0; i<cartesian_product->size(); i++) delete cartesian_product->at(i);
	    delete cartesian_product; cartesian_product = NULL;
	}else{
	  computeQuerySubstitutions(cartesian_product,select_expressions,upper_substitutions,from_components,upper_from_components);
	  formula->setFormulas(cartesian_product);
	  for(unsigned int i=0; i<cartesian_product->size(); i++) delete cartesian_product->at(i);
	  delete cartesian_product; cartesian_product = NULL;
	}// if
	
	// TODO: GROUP BY and HAVING

    return formula;
}

void FormulaGenerator::generateFromFormulas(vector<FromComponent *> * from_components)
{
    for(unsigned int i=0; i<from_components->size(); i++){
        map<string, SchemaComponentFormula *>::iterator it;
        it = generated->find(from_components->at(i)->getName());
        if(it == generated->end()) generate(from_components->at(i)->getName());
    }// for
}

vector<Formula *> * FormulaGenerator::calculateCartesianProduct(vector<FromComponent *> * from_components)
{
    vector<Formula *> * result = new vector<Formula *>();

    map<string, SchemaComponentFormula *>::iterator it;
    it = generated->find(from_components->at(0)->getName());

    vector<Formula *> * first_aux_aux = (*it).second->getAllFormulas();
    vector<Formula *> * first_aux = new vector<Formula *>();
    for(unsigned int i=0; i<first_aux_aux->size(); i++){
        first_aux->push_back(first_aux_aux->at(i)->clone());
    }// for
    for(unsigned int i=0; i<first_aux->size(); i++){
        updateSubstitutionsWithRename(first_aux->at(i),from_components->at(0)->getRename());
    }// for

    for(unsigned int i=0; i<first_aux->size(); i++) result->push_back(first_aux->at(i)->clone());
	
	for(unsigned int i=0; i<first_aux->size(); i++) delete first_aux->at(i);
	delete  first_aux; first_aux = NULL;

    for(unsigned int i=1; i<from_components->size(); i++){
        it = generated->find(from_components->at(i)->getName());

        vector<Formula *> * next_formulas_aux = (*it).second->getAllFormulas();
        vector<Formula *> * next_formulas = new vector<Formula *>();
        for(unsigned int j=0; j<next_formulas_aux->size(); j++){
            next_formulas->push_back(next_formulas_aux->at(j)->clone());
        }// for
        for(unsigned int j=0; j<next_formulas->size(); j++){
            updateSubstitutionsWithRename(next_formulas->at(j),from_components->at(i)->getRename());
        }// for

        vector<Formula *> * aux_result = result;
        result = new vector<Formula *>();
        for(unsigned int j=0; j<aux_result->size(); j++){
            for(unsigned int k=0; k<next_formulas->size(); k++){
                vector<Formula *> * to_conjunction = new vector<Formula *>();
                to_conjunction->push_back(aux_result->at(j));
                to_conjunction->push_back(next_formulas->at(k));
                Expression * conjunction = createConjunction(to_conjunction);
                vector<Substitution *> * substitutions = mergeSubstitutions(aux_result->at(j)->getSubstitutions(),next_formulas->at(k)->getSubstitutions());
                Formula * f = new Formula();
                f->setExpression(conjunction);
                f->setSubstitutions(substitutions);
                delete conjunction; conjunction = NULL;
                delete substitutions; substitutions = NULL;

                result->push_back(f);

                f=NULL;
            }// for
        }// for

        for(unsigned int j=0; j<next_formulas->size(); j++) delete next_formulas->at(j);
        delete next_formulas; next_formulas = NULL;
        for(unsigned int j=0; j<aux_result->size(); j++) delete aux_result->at(j);
        delete aux_result; aux_result = NULL;
    }// for

    return result;
}

Expression * FormulaGenerator::createDisjunction(vector<Formula *> * formulas)
{
	if(formulas->size() == 1){
		return formulas->at(0)->getExpression()->clone();
	}// if

	LogicBinaryOperation * result = new LogicBinaryOperation(NULL,"OR",NULL);
	Expression * pointer = result;
	for(int i=0; i<formulas->size()-1; i++){
	    LogicBinaryOperation * casting = dynamic_cast<LogicBinaryOperation *>(pointer);
		casting->setLeftExpression(formulas->at(i)->getExpression());
		if(i == formulas->size()-2){
            casting->setRightExpression(formulas->at(i+1)->getExpression());
		}else{
            LogicBinaryOperation * aux = new LogicBinaryOperation(NULL,"OR",NULL);
            casting->setRightExpression(aux);
            delete aux; aux = NULL;
		}// if-else
		pointer = casting->getRightExpression();
	}// for

	return result;
}

Expression * FormulaGenerator::createConjunction(vector<Formula *> * formulas)
{
	if(formulas->size() == 1){
		return formulas->at(0)->getExpression()->clone();
	}// if

	LogicBinaryOperation * result = new LogicBinaryOperation(NULL,"AND",NULL);
	Expression * pointer = result;
	for(int i=0; i<formulas->size()-1; i++){
	    LogicBinaryOperation * casting = dynamic_cast<LogicBinaryOperation *>(pointer);
		casting->setLeftExpression(formulas->at(i)->getExpression());
		if(i == formulas->size()-2){
            casting->setRightExpression(formulas->at(i+1)->getExpression());
		}else{
            LogicBinaryOperation * aux = new LogicBinaryOperation(NULL,"AND",NULL);
            casting->setRightExpression(aux);
            delete aux; aux = NULL;
		}// if-else
		pointer = casting->getRightExpression();
	}// for

	return result;
}

void FormulaGenerator::updateSubstitutionsWithRename(Formula * formula, const string & rename)
{
    vector<Substitution *> * substitutions = formula->getSubstitutions();
    for(unsigned int i=0; i<substitutions->size(); i++){
        Substitution * s = substitutions->at(i);
        string substituted = s->getSubstituted();
        string from_dot = substituted.substr(substituted.find_first_of("."));
        s->setSubstituted(rename + from_dot);
    }// for
}

vector<Substitution *> * FormulaGenerator::mergeSubstitutions(vector<Substitution *> * s1, vector<Substitution*> * s2)
{
    vector<Substitution *> * result = new vector<Substitution *>();
    for(int i=0; i<s1->size(); i++) result->push_back(s1->at(i)->clone());
    for(int i=0; i<s2->size(); i++) result->push_back(s2->at(i)->clone());
    return result;
}

vector<Formula *> * FormulaGenerator::generateWhereFormula(Expression * where_expression,vector<Formula *> * cartesian_product,vector<Substitution *> * upper_substitutions,vector<FromComponent *> * from_components, vector<FromComponent *> * upper_from_components)
{
    vector<Formula *> * result_without_exists = new vector<Formula *>();
    for(unsigned int i=0; i<cartesian_product->size(); i++){
        vector<Substitution *> * substitutions = cartesian_product->at(i)->getSubstitutions();
        Expression * replaced = replaceColumnReferenceByExpression(where_expression,substitutions,upper_substitutions,from_components,upper_from_components);

        Formula * f_replaced = new Formula();
        f_replaced->setExpression(replaced);
        vector<Formula *> * to_conjunction = new vector<Formula *>();
        to_conjunction->push_back(cartesian_product->at(i));
        to_conjunction->push_back(f_replaced);

        Expression * conjunction = createConjunction(to_conjunction);
        vector<Substitution *> * merged_substitutions = new vector<Substitution *>();
        for(unsigned int j=0; j<substitutions->size(); j++){
            merged_substitutions->push_back(substitutions->at(j)->clone());
        }// for
        Formula * to_result = new Formula();
        to_result->setExpression(conjunction);
        to_result->setSubstitutions(merged_substitutions);

        delete replaced; replaced = NULL;

        delete f_replaced; f_replaced = NULL;

        //for(unsigned int j=0; j<to_conjunction->size(); j++) delete to_conjunction->at(j);
        delete to_conjunction; to_conjunction = NULL;

        delete conjunction; conjunction = NULL;

        for(unsigned int j=0; j<merged_substitutions->size(); j++) delete merged_substitutions->at(j);
        delete merged_substitutions; merged_substitutions = NULL;

        result_without_exists->push_back(to_result);

        to_result = NULL;
    }// for

    // COMPUTE EXISTS
    //

    vector<Formula *> * result_with_exists= new vector<Formula *>();
    for(unsigned int i=0; i<result_without_exists->size(); i++){
        Expression * expression = result_without_exists->at(i)->getExpression()->clone();
        vector<Substitution *> * actual_substitutions = result_without_exists->at(i)->getSubstitutions();
        vector<Substitution *> * to_pass = new vector<Substitution *>();
        for(unsigned int j=0; j<upper_substitutions->size(); j++) to_pass->push_back(upper_substitutions->at(j)->clone());
        for(unsigned int j=0; j<actual_substitutions->size(); j++) to_pass->push_back(actual_substitutions->at(j)->clone());
        Expression * resolved = resolveExists(expression,to_pass,upper_from_components); // for each formula of cartesian_product_and_where
        for(unsigned int j=0; j<to_pass->size(); j++) delete to_pass->at(j);
        delete to_pass; to_pass = NULL;
        delete expression; expression = NULL;
        result_with_exists->push_back(new Formula(resolved, result_without_exists->at(i)->getSubstitutions()));
        delete resolved; resolved = NULL;
    }// for

    for(unsigned int i=0; i<result_without_exists->size(); i++) delete result_without_exists->at(i);
    delete result_without_exists; result_without_exists = NULL;

    return result_with_exists;
}

void FormulaGenerator::computeQuerySubstitutions(vector<Formula *> * formulas, vector<Expression *> * select_expressions, vector<Substitution *> * upper_substitutions,vector<FromComponent *> * from_components,vector<FromComponent *> * upper_from_components)
{
    for(unsigned int i=0; i<formulas->size(); i++) {
        vector<Substitution *> * substitutions = new vector<Substitution *>();
        for(unsigned int j=0; j<select_expressions->size(); j++){
            Expression * replaced = replaceColumnReferenceByExpression(select_expressions->at(j),formulas->at(i)->getSubstitutions(),upper_substitutions,from_components,upper_from_components);
            substitutions->push_back(new Substitution(select_expressions->at(j)->toString(),replaced));
            delete replaced; replaced = NULL;
        }// for
        formulas->at(i)->setSubstitutions(substitutions);

        for(unsigned int j=0; j<substitutions->size(); j++){
            delete substitutions->at(j);
        }//for
        delete substitutions; substitutions = NULL;

    }// for
}

Expression * FormulaGenerator::replaceColumnReferenceByExpression(Expression * expression, vector<Substitution *> * substitutions, vector<Substitution *> * upper_substitutions, vector<FromComponent *> * from_components,vector<FromComponent *> * upper_from_components)
{
  Expression * result = expression->clone();
  Expression * pointer = result;
  ColumnReference * cr = dynamic_cast<ColumnReference *>(pointer);
Expression * substitution = NULL;
if(cr != NULL){
  if(cr->getTableId() == ""){
    string table_name = searchForTable(cr->getColumnId(),from_components,upper_from_components);
    substitution = searchSubstitution(table_name+"."+cr->getColumnId(),substitutions,upper_substitutions);
  }
  else substitution = searchSubstitution(cr->getTableId()+"."+cr->getColumnId(),substitutions,upper_substitutions);
  //    delete result; result = NULL;
 }
if (substitution!=NULL){
  pointer = substitution->clone();
  return pointer;
 }
LogicBinaryOperation * lbe = dynamic_cast<LogicBinaryOperation *>(pointer);
if(lbe != NULL){
  Expression * exprr = lbe->getRightExpression();
  lbe->setRightExpression(replaceColumnReferenceByExpression(exprr,substitutions, upper_substitutions, from_components, upper_from_components));
  Expression * exprl = lbe->getLeftExpression();
  lbe->setLeftExpression(replaceColumnReferenceByExpression(exprl,substitutions, upper_substitutions, from_components, upper_from_components));
 }
LogicUnaryOperation * lue = dynamic_cast<LogicUnaryOperation *>(pointer);
if(lue != NULL){
  Expression* expr = lue->getExpression();
  lue->setExpression(replaceColumnReferenceByExpression(expr,substitutions, upper_substitutions, from_components, upper_from_components));
 }
NumericBinaryOperation * nbe = dynamic_cast<NumericBinaryOperation *>(pointer);
if(nbe != NULL){
  Expression * exprr = nbe->getRightExpression();
  nbe->setRightExpression(replaceColumnReferenceByExpression(exprr,substitutions, upper_substitutions, from_components, upper_from_components));
  Expression * exprl = nbe->getLeftExpression();
  nbe->setLeftExpression(replaceColumnReferenceByExpression(exprl,substitutions, upper_substitutions, from_components, upper_from_components));
 }
NumericUnaryOperation * nue = dynamic_cast<NumericUnaryOperation *>(pointer);
if(nue != NULL){
  Expression* expr = nue->getExpression();
  nue->setExpression(replaceColumnReferenceByExpression(expr,substitutions, upper_substitutions, from_components, upper_from_components));
 }
//return result
return pointer;
}

string FormulaGenerator::searchForTable(const string & column, vector<FromComponent *> * from_components, vector<FromComponent *> * upper_from_components)
{
    bool finded = false;
    unsigned int i=0;
    string table_name = "";
    while(!finded && i<from_components->size()){
        SchemaComponent * component = NULL;
        schema->get(from_components->at(i)->getName(),component);
        vector<Column *> * columns = component->getColumns()->getColumns();
        unsigned int j=0;
        while(!finded && j<columns->size()){
            if(columns->at(j)->getName() == column){
                table_name = from_components->at(i)->getRename();
                finded = true;
            }// if
            j++;
        }// while
        i++;
    }// while

    if(finded) return table_name;

    i=0;
    while(!finded && i<upper_from_components->size()){
        SchemaComponent * component = NULL;
        schema->get(upper_from_components->at(i)->getName(),component);
        vector<Column *> * columns = component->getColumns()->getColumns();
        unsigned int j=0;
        while(!finded && j<columns->size()){
            if(columns->at(j)->getName() == column){
                table_name = from_components->at(i)->getRename();
                finded = true;
            }// if
            j++;
        }// while
        i++;
    }// while

    return table_name;
}

Expression * FormulaGenerator::searchSubstitution(const string & to_search, vector<Substitution *> * substitutions, vector<Substitution *> * upper_substitutions)
{
    bool finded = false;
    unsigned int i=0;
    Expression * substitution = NULL;
    while(!finded && i<substitutions->size()){
        if(to_search == substitutions->at(i)->getSubstituted()){
            substitution = substitutions->at(i)->getSubstitution();
            finded = true;
        }// if
        i++;
    }// while

    if(!finded){
        i = 0;
        while(!finded && i<upper_substitutions->size()){
            if(to_search == upper_substitutions->at(i)->getSubstituted()){
                substitution = upper_substitutions->at(i)->getSubstitution();
                finded = true;
            }// if
            i++;
        }// while
    }// if

    return substitution;
}

Expression * FormulaGenerator::resolveExists(Expression * expression, vector<Substitution *> * upper_substitutions, vector<FromComponent *> * upper_components)
{
	Expression * result = expression->clone();
	Expression * pointer = result;

	ExistsExpression * ee = dynamic_cast<ExistsExpression *>(pointer);
    if(ee != NULL){
		SchemaComponentFormula * eesc = generate(ee->getQuery(),upper_substitutions,upper_components);
		vector<Formula *> * formulas = eesc->getAllFormulas();
		Expression * disjunction = createDisjunction(formulas);
        delete result; result = NULL;
		delete eesc; eesc = NULL; formulas = NULL;
        pointer = NULL;
		return disjunction;
    }//if

	stack<Expression *> lifo;
	lifo.push(pointer);
	while(!lifo.empty()){
		pointer = lifo.top();
		lifo.pop();
		LogicBinaryOperation * lbe = dynamic_cast<LogicBinaryOperation *>(pointer);
		if(lbe != NULL){
			ExistsExpression * eer = dynamic_cast<ExistsExpression *>(lbe->getRightExpression());
			if(eer != NULL){
				SchemaComponentFormula * eesc = generate(eer->getQuery(),upper_substitutions,upper_components);
                vector<Formula *> * formulas = eesc->getAllFormulas();
                Expression * disjunction = createDisjunction(formulas);
				lbe->setRightExpression(disjunction);
				delete disjunction; disjunction = NULL;
				delete eesc; eesc = NULL; formulas = NULL;
			}else{
				lifo.push(lbe->getRightExpression());
			}// if-else

			ExistsExpression * eel = dynamic_cast<ExistsExpression *>(lbe->getLeftExpression());
			if(eel != NULL){
				SchemaComponentFormula * eesc = generate(eel->getQuery(),upper_substitutions,upper_components);
                vector<Formula *> * formulas = eesc->getAllFormulas();
                Expression * disjunction = createDisjunction(formulas);
				lbe->setLeftExpression(disjunction);
				delete disjunction; disjunction = NULL;
				delete eesc; eesc = NULL; formulas = NULL;
			}else{
				lifo.push(lbe->getLeftExpression());
			}// if-else
		}else{
			LogicUnaryOperation * lue = dynamic_cast<LogicUnaryOperation *>(pointer);
			if(lue != NULL){
                ExistsExpression * ee = dynamic_cast<ExistsExpression *>(lue->getExpression());
				if(ee != NULL){
					SchemaComponentFormula * eesc = generate(ee->getQuery(),upper_substitutions,upper_components);
                    vector<Formula *> * formulas = eesc->getAllFormulas();
                    Expression * disjunction = createDisjunction(formulas);
					lue->setExpression(disjunction);
                    delete disjunction; disjunction = NULL;
					delete eesc; eesc = NULL; formulas = NULL;
				}else{
					lifo.push(lue->getExpression());
				}// if-else
			}else{
				// NOTHING TO DO
            }// if-else
        }// if-else
	}// while
	return result;
}
